weak-precond-send-p(es;T;A;l;tg;a;ds;P;f)
== (x:Id. vartype(source(l);x)  ds(x)?Top)
== & e@source(l). kind(e) = locl(a)  valtype(e)  A
== & (e:E. kind(e) = rcv(l,tg)  valtype(e)  T)
== & (e':E.
== & (kind(e') = rcv(l,tg)
== & ( kind(sender(e')) = locl(a)
== & ( & P((state when sender(e')),val(sender(e')))
== & ( & & val(e') = f((state when sender(e')),val(sender(e'))))
== & & e@source(l).
== & & e':E.
== & & e c e'
== & & & kind(e') = rcv(l,tg) & e  sender(e') 
== & & &  loc(e') = source(l) & (v:A. P(state after e',v)) 

latex

---

clarification:

weak-precond-send-p(es;T;A;l;tg;a;ds;P;f)
== (x:Id. es-vartype(es; source(l); x)  fpf-cap(ds;IdDeq;x;Top))
== & alle-at(es;source(l);e.es-kind(es; e) = locl(a)  Knd  es-valtype(es; e)  A)
== & (e:es-E(es). es-kind(es; e) = rcv(l,tg)  Knd  es-valtype(es; e)  T)
== & (e':es-E(es).
== & (es-kind(es; e') = rcv(l,tg)  Knd
== & ( es-kind(es; es-sender(es; e')) = locl(a)  Knd
== & ( & P(es-state-when(es;es-sender(es; e')),es-val(es; es-sender(es; e')))
== & ( & & es-val(es; e')
== & ( & & =
== & ( & & f(es-state-when(es;es-sender(es; e')),es-val(es; es-sender(es; e')))
== & ( & &  T)
== & & alle-at(es;source(l);e.e':es-E(es).
== & & es-causle(es;e;e')
== & & & es-kind(es; e') = rcv(l,tg)  Knd & es-le(es;e;es-sender(es; e'))
== & & &  es-loc(es; e') = source(l)  Id & (v:A. P(es-state-after(es;e'),v))) 

latex

Definitions	vartype(i;x), f(x)?z, IdDeq, Top, valtype(e), P  Q, locl(a), (state when e), val(e), e@i. P(e), x:A. B(x), E, P & Q, e c e', P  Q, Knd, kind(e), rcv(l,tg), e  e' , sender(e), A & B, s = t, Id, loc(e), source(l), x:A. B(x), A, f(a), state after e
FDL editor aliases	weak-precond-send-p